The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CdtProblem
    ↳3 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳4 CdtProblem
    ↳5 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳6 CdtProblem
    ↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 129 ms)
    ↳8 CdtProblem
    ↳9 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 17 ms)
    ↳10 CdtProblem
    ↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 131 ms)
    ↳12 CdtProblem
    ↳13 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳14 CdtProblem
    ↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 106 ms)
    ↳16 CdtProblem
    ↳17 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳18 CdtProblem
    ↳19 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 6 ms)
    ↳20 CdtProblem
    ↳21 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)
    ↳22 CdtProblem
↳23 CpxTrsMatchBoundsTAProof (⇔, 0 ms)
↳24 BOUNDS(O(1), O(n^1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

f(x, f(s(s(y)), f(z, w))) → f(s(x), f(y, f(s(z), w)))
L(f(s(s(y)), f(z, w))) → L(f(s(0), f(y, f(s(z), w))))
f(x, f(s(s(y)), nil)) → f(s(x), f(y, f(s(0), nil)))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, f(s(s(z1)), f(z2, z3))) → f(s(z0), f(z1, f(s(z2), z3)))
f(z0, f(s(s(z1)), nil)) → f(s(z0), f(z1, f(s(0), nil)))
L(f(s(s(z0)), f(z1, z2))) → L(f(s(0), f(z0, f(s(z1), z2))))
Tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
F(z0, f(s(s(z1)), nil)) → c1(F(s(z0), f(z1, f(s(0), nil))), F(z1, f(s(0), nil)), F(s(0), nil))
L'(f(s(s(z0)), f(z1, z2))) → c2(L'(f(s(0), f(z0, f(s(z1), z2)))), F(s(0), f(z0, f(s(z1), z2))), F(z0, f(s(z1), z2)), F(s(z1), z2))
S tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
F(z0, f(s(s(z1)), nil)) → c1(F(s(z0), f(z1, f(s(0), nil))), F(z1, f(s(0), nil)), F(s(0), nil))
L'(f(s(s(z0)), f(z1, z2))) → c2(L'(f(s(0), f(z0, f(s(z1), z2)))), F(s(0), f(z0, f(s(z1), z2))), F(z0, f(s(z1), z2)), F(s(z1), z2))
K tuples:none
Defined Rule Symbols:

f, L

Defined Pair Symbols:

F, L'

Compound Symbols:

c, c1, c2

(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F(z0, f(s(s(z1)), nil)) → c1(F(s(z0), f(z1, f(s(0), nil))), F(z1, f(s(0), nil)), F(s(0), nil)) by

F(x0, f(s(s(x1)), nil)) → c1(F(s(x0), f(x1, f(s(0), nil))))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, f(s(s(z1)), f(z2, z3))) → f(s(z0), f(z1, f(s(z2), z3)))
f(z0, f(s(s(z1)), nil)) → f(s(z0), f(z1, f(s(0), nil)))
L(f(s(s(z0)), f(z1, z2))) → L(f(s(0), f(z0, f(s(z1), z2))))
Tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
L'(f(s(s(z0)), f(z1, z2))) → c2(L'(f(s(0), f(z0, f(s(z1), z2)))), F(s(0), f(z0, f(s(z1), z2))), F(z0, f(s(z1), z2)), F(s(z1), z2))
F(x0, f(s(s(x1)), nil)) → c1(F(s(x0), f(x1, f(s(0), nil))))
S tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
L'(f(s(s(z0)), f(z1, z2))) → c2(L'(f(s(0), f(z0, f(s(z1), z2)))), F(s(0), f(z0, f(s(z1), z2))), F(z0, f(s(z1), z2)), F(s(z1), z2))
F(x0, f(s(s(x1)), nil)) → c1(F(s(x0), f(x1, f(s(0), nil))))
K tuples:none
Defined Rule Symbols:

f, L

Defined Pair Symbols:

F, L'

Compound Symbols:

c, c2, c1

(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace L'(f(s(s(z0)), f(z1, z2))) → c2(L'(f(s(0), f(z0, f(s(z1), z2)))), F(s(0), f(z0, f(s(z1), z2))), F(z0, f(s(z1), z2)), F(s(z1), z2)) by

L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(z0)), f(s(z1), f(z2, z3)))) → c2(L'(f(s(0), f(s(z0), f(z1, f(s(z2), z3))))), F(s(0), f(z0, f(s(s(z1)), f(z2, z3)))), F(z0, f(s(s(z1)), f(z2, z3))), F(s(s(z1)), f(z2, z3)))
L'(f(s(s(z0)), f(s(z1), nil))) → c2(L'(f(s(0), f(s(z0), f(z1, f(s(0), nil))))), F(s(0), f(z0, f(s(s(z1)), nil))), F(z0, f(s(s(z1)), nil)), F(s(s(z1)), nil))
L'(f(s(s(x0)), f(x1, x2))) → c2(F(s(x1), x2))

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, f(s(s(z1)), f(z2, z3))) → f(s(z0), f(z1, f(s(z2), z3)))
f(z0, f(s(s(z1)), nil)) → f(s(z0), f(z1, f(s(0), nil)))
L(f(s(s(z0)), f(z1, z2))) → L(f(s(0), f(z0, f(s(z1), z2))))
Tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
F(x0, f(s(s(x1)), nil)) → c1(F(s(x0), f(x1, f(s(0), nil))))
L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(z0)), f(s(z1), f(z2, z3)))) → c2(L'(f(s(0), f(s(z0), f(z1, f(s(z2), z3))))), F(s(0), f(z0, f(s(s(z1)), f(z2, z3)))), F(z0, f(s(s(z1)), f(z2, z3))), F(s(s(z1)), f(z2, z3)))
L'(f(s(s(z0)), f(s(z1), nil))) → c2(L'(f(s(0), f(s(z0), f(z1, f(s(0), nil))))), F(s(0), f(z0, f(s(s(z1)), nil))), F(z0, f(s(s(z1)), nil)), F(s(s(z1)), nil))
L'(f(s(s(x0)), f(x1, x2))) → c2(F(s(x1), x2))
S tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
F(x0, f(s(s(x1)), nil)) → c1(F(s(x0), f(x1, f(s(0), nil))))
L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(z0)), f(s(z1), f(z2, z3)))) → c2(L'(f(s(0), f(s(z0), f(z1, f(s(z2), z3))))), F(s(0), f(z0, f(s(s(z1)), f(z2, z3)))), F(z0, f(s(s(z1)), f(z2, z3))), F(s(s(z1)), f(z2, z3)))
L'(f(s(s(z0)), f(s(z1), nil))) → c2(L'(f(s(0), f(s(z0), f(z1, f(s(0), nil))))), F(s(0), f(z0, f(s(s(z1)), nil))), F(z0, f(s(s(z1)), nil)), F(s(s(z1)), nil))
L'(f(s(s(x0)), f(x1, x2))) → c2(F(s(x1), x2))
K tuples:none
Defined Rule Symbols:

f, L

Defined Pair Symbols:

F, L'

Compound Symbols:

c, c1, c2, c2

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

L'(f(s(s(x0)), f(x1, x2))) → c2(F(s(x1), x2))
We considered the (Usable) Rules:

f(z0, f(s(s(z1)), nil)) → f(s(z0), f(z1, f(s(0), nil)))
f(z0, f(s(s(z1)), f(z2, z3))) → f(s(z0), f(z1, f(s(z2), z3)))
And the Tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
F(x0, f(s(s(x1)), nil)) → c1(F(s(x0), f(x1, f(s(0), nil))))
L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(z0)), f(s(z1), f(z2, z3)))) → c2(L'(f(s(0), f(s(z0), f(z1, f(s(z2), z3))))), F(s(0), f(z0, f(s(s(z1)), f(z2, z3)))), F(z0, f(s(s(z1)), f(z2, z3))), F(s(s(z1)), f(z2, z3)))
L'(f(s(s(z0)), f(s(z1), nil))) → c2(L'(f(s(0), f(s(z0), f(z1, f(s(0), nil))))), F(s(0), f(z0, f(s(s(z1)), nil))), F(z0, f(s(s(z1)), nil)), F(s(s(z1)), nil))
L'(f(s(s(x0)), f(x1, x2))) → c2(F(s(x1), x2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [3]   
POL(F(x1, x2)) = 0   
POL(L'(x1)) = [1]   
POL(c(x1, x2, x3)) = x1 + x2 + x3   
POL(c1(x1)) = x1   
POL(c2(x1)) = x1   
POL(c2(x1, x2, x3, x4)) = x1 + x2 + x3 + x4   
POL(f(x1, x2)) = [2]   
POL(nil) = [4]   
POL(s(x1)) = 0   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, f(s(s(z1)), f(z2, z3))) → f(s(z0), f(z1, f(s(z2), z3)))
f(z0, f(s(s(z1)), nil)) → f(s(z0), f(z1, f(s(0), nil)))
L(f(s(s(z0)), f(z1, z2))) → L(f(s(0), f(z0, f(s(z1), z2))))
Tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
F(x0, f(s(s(x1)), nil)) → c1(F(s(x0), f(x1, f(s(0), nil))))
L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(z0)), f(s(z1), f(z2, z3)))) → c2(L'(f(s(0), f(s(z0), f(z1, f(s(z2), z3))))), F(s(0), f(z0, f(s(s(z1)), f(z2, z3)))), F(z0, f(s(s(z1)), f(z2, z3))), F(s(s(z1)), f(z2, z3)))
L'(f(s(s(z0)), f(s(z1), nil))) → c2(L'(f(s(0), f(s(z0), f(z1, f(s(0), nil))))), F(s(0), f(z0, f(s(s(z1)), nil))), F(z0, f(s(s(z1)), nil)), F(s(s(z1)), nil))
L'(f(s(s(x0)), f(x1, x2))) → c2(F(s(x1), x2))
S tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
F(x0, f(s(s(x1)), nil)) → c1(F(s(x0), f(x1, f(s(0), nil))))
L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(z0)), f(s(z1), f(z2, z3)))) → c2(L'(f(s(0), f(s(z0), f(z1, f(s(z2), z3))))), F(s(0), f(z0, f(s(s(z1)), f(z2, z3)))), F(z0, f(s(s(z1)), f(z2, z3))), F(s(s(z1)), f(z2, z3)))
L'(f(s(s(z0)), f(s(z1), nil))) → c2(L'(f(s(0), f(s(z0), f(z1, f(s(0), nil))))), F(s(0), f(z0, f(s(s(z1)), nil))), F(z0, f(s(s(z1)), nil)), F(s(s(z1)), nil))
K tuples:

L'(f(s(s(x0)), f(x1, x2))) → c2(F(s(x1), x2))
Defined Rule Symbols:

f, L

Defined Pair Symbols:

F, L'

Compound Symbols:

c, c1, c2, c2

(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace L'(f(s(s(z0)), f(s(z1), f(z2, z3)))) → c2(L'(f(s(0), f(s(z0), f(z1, f(s(z2), z3))))), F(s(0), f(z0, f(s(s(z1)), f(z2, z3)))), F(z0, f(s(s(z1)), f(z2, z3))), F(s(s(z1)), f(z2, z3))) by

L'(f(s(s(s(z1))), f(s(z2), f(x2, x3)))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(x2), x3))))), F(s(0), f(s(z1), f(s(s(z2)), f(x2, x3)))), F(s(z1), f(s(s(z2)), f(x2, x3))), F(s(s(z2)), f(x2, x3)))
L'(f(s(s(x0)), f(s(z0), f(s(z1), f(z2, z3))))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(z2), z3)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), f(z2, z3))))), F(x0, f(s(s(z0)), f(s(z1), f(z2, z3)))), F(s(s(z0)), f(s(z1), f(z2, z3))))
L'(f(s(s(x0)), f(s(z0), f(s(z1), nil)))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(0), nil)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), nil)))), F(x0, f(s(s(z0)), f(s(z1), nil))), F(s(s(z0)), f(s(z1), nil)))
L'(f(s(s(x0)), f(s(x1), f(x2, x3)))) → c2(F(s(0), f(x0, f(s(s(x1)), f(x2, x3)))), F(x0, f(s(s(x1)), f(x2, x3))), F(s(s(x1)), f(x2, x3)))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, f(s(s(z1)), f(z2, z3))) → f(s(z0), f(z1, f(s(z2), z3)))
f(z0, f(s(s(z1)), nil)) → f(s(z0), f(z1, f(s(0), nil)))
L(f(s(s(z0)), f(z1, z2))) → L(f(s(0), f(z0, f(s(z1), z2))))
Tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
F(x0, f(s(s(x1)), nil)) → c1(F(s(x0), f(x1, f(s(0), nil))))
L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(z0)), f(s(z1), nil))) → c2(L'(f(s(0), f(s(z0), f(z1, f(s(0), nil))))), F(s(0), f(z0, f(s(s(z1)), nil))), F(z0, f(s(s(z1)), nil)), F(s(s(z1)), nil))
L'(f(s(s(x0)), f(x1, x2))) → c2(F(s(x1), x2))
L'(f(s(s(s(z1))), f(s(z2), f(x2, x3)))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(x2), x3))))), F(s(0), f(s(z1), f(s(s(z2)), f(x2, x3)))), F(s(z1), f(s(s(z2)), f(x2, x3))), F(s(s(z2)), f(x2, x3)))
L'(f(s(s(x0)), f(s(z0), f(s(z1), f(z2, z3))))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(z2), z3)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), f(z2, z3))))), F(x0, f(s(s(z0)), f(s(z1), f(z2, z3)))), F(s(s(z0)), f(s(z1), f(z2, z3))))
L'(f(s(s(x0)), f(s(z0), f(s(z1), nil)))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(0), nil)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), nil)))), F(x0, f(s(s(z0)), f(s(z1), nil))), F(s(s(z0)), f(s(z1), nil)))
L'(f(s(s(x0)), f(s(x1), f(x2, x3)))) → c2(F(s(0), f(x0, f(s(s(x1)), f(x2, x3)))), F(x0, f(s(s(x1)), f(x2, x3))), F(s(s(x1)), f(x2, x3)))
S tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
F(x0, f(s(s(x1)), nil)) → c1(F(s(x0), f(x1, f(s(0), nil))))
L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(z0)), f(s(z1), nil))) → c2(L'(f(s(0), f(s(z0), f(z1, f(s(0), nil))))), F(s(0), f(z0, f(s(s(z1)), nil))), F(z0, f(s(s(z1)), nil)), F(s(s(z1)), nil))
L'(f(s(s(s(z1))), f(s(z2), f(x2, x3)))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(x2), x3))))), F(s(0), f(s(z1), f(s(s(z2)), f(x2, x3)))), F(s(z1), f(s(s(z2)), f(x2, x3))), F(s(s(z2)), f(x2, x3)))
L'(f(s(s(x0)), f(s(z0), f(s(z1), f(z2, z3))))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(z2), z3)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), f(z2, z3))))), F(x0, f(s(s(z0)), f(s(z1), f(z2, z3)))), F(s(s(z0)), f(s(z1), f(z2, z3))))
L'(f(s(s(x0)), f(s(z0), f(s(z1), nil)))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(0), nil)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), nil)))), F(x0, f(s(s(z0)), f(s(z1), nil))), F(s(s(z0)), f(s(z1), nil)))
L'(f(s(s(x0)), f(s(x1), f(x2, x3)))) → c2(F(s(0), f(x0, f(s(s(x1)), f(x2, x3)))), F(x0, f(s(s(x1)), f(x2, x3))), F(s(s(x1)), f(x2, x3)))
K tuples:

L'(f(s(s(x0)), f(x1, x2))) → c2(F(s(x1), x2))
Defined Rule Symbols:

f, L

Defined Pair Symbols:

F, L'

Compound Symbols:

c, c1, c2, c2, c2

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

L'(f(s(s(x0)), f(s(x1), f(x2, x3)))) → c2(F(s(0), f(x0, f(s(s(x1)), f(x2, x3)))), F(x0, f(s(s(x1)), f(x2, x3))), F(s(s(x1)), f(x2, x3)))
We considered the (Usable) Rules:

f(z0, f(s(s(z1)), nil)) → f(s(z0), f(z1, f(s(0), nil)))
f(z0, f(s(s(z1)), f(z2, z3))) → f(s(z0), f(z1, f(s(z2), z3)))
And the Tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
F(x0, f(s(s(x1)), nil)) → c1(F(s(x0), f(x1, f(s(0), nil))))
L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(z0)), f(s(z1), nil))) → c2(L'(f(s(0), f(s(z0), f(z1, f(s(0), nil))))), F(s(0), f(z0, f(s(s(z1)), nil))), F(z0, f(s(s(z1)), nil)), F(s(s(z1)), nil))
L'(f(s(s(x0)), f(x1, x2))) → c2(F(s(x1), x2))
L'(f(s(s(s(z1))), f(s(z2), f(x2, x3)))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(x2), x3))))), F(s(0), f(s(z1), f(s(s(z2)), f(x2, x3)))), F(s(z1), f(s(s(z2)), f(x2, x3))), F(s(s(z2)), f(x2, x3)))
L'(f(s(s(x0)), f(s(z0), f(s(z1), f(z2, z3))))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(z2), z3)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), f(z2, z3))))), F(x0, f(s(s(z0)), f(s(z1), f(z2, z3)))), F(s(s(z0)), f(s(z1), f(z2, z3))))
L'(f(s(s(x0)), f(s(z0), f(s(z1), nil)))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(0), nil)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), nil)))), F(x0, f(s(s(z0)), f(s(z1), nil))), F(s(s(z0)), f(s(z1), nil)))
L'(f(s(s(x0)), f(s(x1), f(x2, x3)))) → c2(F(s(0), f(x0, f(s(s(x1)), f(x2, x3)))), F(x0, f(s(s(x1)), f(x2, x3))), F(s(s(x1)), f(x2, x3)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [3]   
POL(F(x1, x2)) = 0   
POL(L'(x1)) = [1]   
POL(c(x1, x2, x3)) = x1 + x2 + x3   
POL(c1(x1)) = x1   
POL(c2(x1)) = x1   
POL(c2(x1, x2, x3)) = x1 + x2 + x3   
POL(c2(x1, x2, x3, x4)) = x1 + x2 + x3 + x4   
POL(f(x1, x2)) = [3]   
POL(nil) = [3]   
POL(s(x1)) = 0   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, f(s(s(z1)), f(z2, z3))) → f(s(z0), f(z1, f(s(z2), z3)))
f(z0, f(s(s(z1)), nil)) → f(s(z0), f(z1, f(s(0), nil)))
L(f(s(s(z0)), f(z1, z2))) → L(f(s(0), f(z0, f(s(z1), z2))))
Tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
F(x0, f(s(s(x1)), nil)) → c1(F(s(x0), f(x1, f(s(0), nil))))
L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(z0)), f(s(z1), nil))) → c2(L'(f(s(0), f(s(z0), f(z1, f(s(0), nil))))), F(s(0), f(z0, f(s(s(z1)), nil))), F(z0, f(s(s(z1)), nil)), F(s(s(z1)), nil))
L'(f(s(s(x0)), f(x1, x2))) → c2(F(s(x1), x2))
L'(f(s(s(s(z1))), f(s(z2), f(x2, x3)))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(x2), x3))))), F(s(0), f(s(z1), f(s(s(z2)), f(x2, x3)))), F(s(z1), f(s(s(z2)), f(x2, x3))), F(s(s(z2)), f(x2, x3)))
L'(f(s(s(x0)), f(s(z0), f(s(z1), f(z2, z3))))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(z2), z3)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), f(z2, z3))))), F(x0, f(s(s(z0)), f(s(z1), f(z2, z3)))), F(s(s(z0)), f(s(z1), f(z2, z3))))
L'(f(s(s(x0)), f(s(z0), f(s(z1), nil)))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(0), nil)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), nil)))), F(x0, f(s(s(z0)), f(s(z1), nil))), F(s(s(z0)), f(s(z1), nil)))
L'(f(s(s(x0)), f(s(x1), f(x2, x3)))) → c2(F(s(0), f(x0, f(s(s(x1)), f(x2, x3)))), F(x0, f(s(s(x1)), f(x2, x3))), F(s(s(x1)), f(x2, x3)))
S tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
F(x0, f(s(s(x1)), nil)) → c1(F(s(x0), f(x1, f(s(0), nil))))
L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(z0)), f(s(z1), nil))) → c2(L'(f(s(0), f(s(z0), f(z1, f(s(0), nil))))), F(s(0), f(z0, f(s(s(z1)), nil))), F(z0, f(s(s(z1)), nil)), F(s(s(z1)), nil))
L'(f(s(s(s(z1))), f(s(z2), f(x2, x3)))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(x2), x3))))), F(s(0), f(s(z1), f(s(s(z2)), f(x2, x3)))), F(s(z1), f(s(s(z2)), f(x2, x3))), F(s(s(z2)), f(x2, x3)))
L'(f(s(s(x0)), f(s(z0), f(s(z1), f(z2, z3))))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(z2), z3)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), f(z2, z3))))), F(x0, f(s(s(z0)), f(s(z1), f(z2, z3)))), F(s(s(z0)), f(s(z1), f(z2, z3))))
L'(f(s(s(x0)), f(s(z0), f(s(z1), nil)))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(0), nil)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), nil)))), F(x0, f(s(s(z0)), f(s(z1), nil))), F(s(s(z0)), f(s(z1), nil)))
K tuples:

L'(f(s(s(x0)), f(x1, x2))) → c2(F(s(x1), x2))
L'(f(s(s(x0)), f(s(x1), f(x2, x3)))) → c2(F(s(0), f(x0, f(s(s(x1)), f(x2, x3)))), F(x0, f(s(s(x1)), f(x2, x3))), F(s(s(x1)), f(x2, x3)))
Defined Rule Symbols:

f, L

Defined Pair Symbols:

F, L'

Compound Symbols:

c, c1, c2, c2, c2

(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace L'(f(s(s(z0)), f(s(z1), nil))) → c2(L'(f(s(0), f(s(z0), f(z1, f(s(0), nil))))), F(s(0), f(z0, f(s(s(z1)), nil))), F(z0, f(s(s(z1)), nil)), F(s(s(z1)), nil)) by

L'(f(s(s(s(z1))), f(s(z2), nil))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(0), nil))))), F(s(0), f(s(z1), f(s(s(z2)), nil))), F(s(z1), f(s(s(z2)), nil)), F(s(s(z2)), nil))
L'(f(s(s(x0)), f(s(x1), nil))) → c2(F(s(0), f(x0, f(s(s(x1)), nil))), F(x0, f(s(s(x1)), nil)))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, f(s(s(z1)), f(z2, z3))) → f(s(z0), f(z1, f(s(z2), z3)))
f(z0, f(s(s(z1)), nil)) → f(s(z0), f(z1, f(s(0), nil)))
L(f(s(s(z0)), f(z1, z2))) → L(f(s(0), f(z0, f(s(z1), z2))))
Tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
F(x0, f(s(s(x1)), nil)) → c1(F(s(x0), f(x1, f(s(0), nil))))
L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(x0)), f(x1, x2))) → c2(F(s(x1), x2))
L'(f(s(s(s(z1))), f(s(z2), f(x2, x3)))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(x2), x3))))), F(s(0), f(s(z1), f(s(s(z2)), f(x2, x3)))), F(s(z1), f(s(s(z2)), f(x2, x3))), F(s(s(z2)), f(x2, x3)))
L'(f(s(s(x0)), f(s(z0), f(s(z1), f(z2, z3))))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(z2), z3)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), f(z2, z3))))), F(x0, f(s(s(z0)), f(s(z1), f(z2, z3)))), F(s(s(z0)), f(s(z1), f(z2, z3))))
L'(f(s(s(x0)), f(s(z0), f(s(z1), nil)))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(0), nil)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), nil)))), F(x0, f(s(s(z0)), f(s(z1), nil))), F(s(s(z0)), f(s(z1), nil)))
L'(f(s(s(x0)), f(s(x1), f(x2, x3)))) → c2(F(s(0), f(x0, f(s(s(x1)), f(x2, x3)))), F(x0, f(s(s(x1)), f(x2, x3))), F(s(s(x1)), f(x2, x3)))
L'(f(s(s(s(z1))), f(s(z2), nil))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(0), nil))))), F(s(0), f(s(z1), f(s(s(z2)), nil))), F(s(z1), f(s(s(z2)), nil)), F(s(s(z2)), nil))
L'(f(s(s(x0)), f(s(x1), nil))) → c2(F(s(0), f(x0, f(s(s(x1)), nil))), F(x0, f(s(s(x1)), nil)))
S tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
F(x0, f(s(s(x1)), nil)) → c1(F(s(x0), f(x1, f(s(0), nil))))
L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(s(z1))), f(s(z2), f(x2, x3)))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(x2), x3))))), F(s(0), f(s(z1), f(s(s(z2)), f(x2, x3)))), F(s(z1), f(s(s(z2)), f(x2, x3))), F(s(s(z2)), f(x2, x3)))
L'(f(s(s(x0)), f(s(z0), f(s(z1), f(z2, z3))))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(z2), z3)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), f(z2, z3))))), F(x0, f(s(s(z0)), f(s(z1), f(z2, z3)))), F(s(s(z0)), f(s(z1), f(z2, z3))))
L'(f(s(s(x0)), f(s(z0), f(s(z1), nil)))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(0), nil)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), nil)))), F(x0, f(s(s(z0)), f(s(z1), nil))), F(s(s(z0)), f(s(z1), nil)))
L'(f(s(s(s(z1))), f(s(z2), nil))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(0), nil))))), F(s(0), f(s(z1), f(s(s(z2)), nil))), F(s(z1), f(s(s(z2)), nil)), F(s(s(z2)), nil))
L'(f(s(s(x0)), f(s(x1), nil))) → c2(F(s(0), f(x0, f(s(s(x1)), nil))), F(x0, f(s(s(x1)), nil)))
K tuples:

L'(f(s(s(x0)), f(x1, x2))) → c2(F(s(x1), x2))
L'(f(s(s(x0)), f(s(x1), f(x2, x3)))) → c2(F(s(0), f(x0, f(s(s(x1)), f(x2, x3)))), F(x0, f(s(s(x1)), f(x2, x3))), F(s(s(x1)), f(x2, x3)))
Defined Rule Symbols:

f, L

Defined Pair Symbols:

F, L'

Compound Symbols:

c, c1, c2, c2, c2, c2

(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

L'(f(s(s(x0)), f(s(x1), nil))) → c2(F(s(0), f(x0, f(s(s(x1)), nil))), F(x0, f(s(s(x1)), nil)))
We considered the (Usable) Rules:

f(z0, f(s(s(z1)), nil)) → f(s(z0), f(z1, f(s(0), nil)))
f(z0, f(s(s(z1)), f(z2, z3))) → f(s(z0), f(z1, f(s(z2), z3)))
And the Tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
F(x0, f(s(s(x1)), nil)) → c1(F(s(x0), f(x1, f(s(0), nil))))
L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(x0)), f(x1, x2))) → c2(F(s(x1), x2))
L'(f(s(s(s(z1))), f(s(z2), f(x2, x3)))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(x2), x3))))), F(s(0), f(s(z1), f(s(s(z2)), f(x2, x3)))), F(s(z1), f(s(s(z2)), f(x2, x3))), F(s(s(z2)), f(x2, x3)))
L'(f(s(s(x0)), f(s(z0), f(s(z1), f(z2, z3))))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(z2), z3)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), f(z2, z3))))), F(x0, f(s(s(z0)), f(s(z1), f(z2, z3)))), F(s(s(z0)), f(s(z1), f(z2, z3))))
L'(f(s(s(x0)), f(s(z0), f(s(z1), nil)))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(0), nil)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), nil)))), F(x0, f(s(s(z0)), f(s(z1), nil))), F(s(s(z0)), f(s(z1), nil)))
L'(f(s(s(x0)), f(s(x1), f(x2, x3)))) → c2(F(s(0), f(x0, f(s(s(x1)), f(x2, x3)))), F(x0, f(s(s(x1)), f(x2, x3))), F(s(s(x1)), f(x2, x3)))
L'(f(s(s(s(z1))), f(s(z2), nil))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(0), nil))))), F(s(0), f(s(z1), f(s(s(z2)), nil))), F(s(z1), f(s(s(z2)), nil)), F(s(s(z2)), nil))
L'(f(s(s(x0)), f(s(x1), nil))) → c2(F(s(0), f(x0, f(s(s(x1)), nil))), F(x0, f(s(s(x1)), nil)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [3]   
POL(F(x1, x2)) = 0   
POL(L'(x1)) = [1]   
POL(c(x1, x2, x3)) = x1 + x2 + x3   
POL(c1(x1)) = x1   
POL(c2(x1)) = x1   
POL(c2(x1, x2)) = x1 + x2   
POL(c2(x1, x2, x3)) = x1 + x2 + x3   
POL(c2(x1, x2, x3, x4)) = x1 + x2 + x3 + x4   
POL(f(x1, x2)) = [3] + x1   
POL(nil) = [2]   
POL(s(x1)) = 0   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, f(s(s(z1)), f(z2, z3))) → f(s(z0), f(z1, f(s(z2), z3)))
f(z0, f(s(s(z1)), nil)) → f(s(z0), f(z1, f(s(0), nil)))
L(f(s(s(z0)), f(z1, z2))) → L(f(s(0), f(z0, f(s(z1), z2))))
Tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
F(x0, f(s(s(x1)), nil)) → c1(F(s(x0), f(x1, f(s(0), nil))))
L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(x0)), f(x1, x2))) → c2(F(s(x1), x2))
L'(f(s(s(s(z1))), f(s(z2), f(x2, x3)))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(x2), x3))))), F(s(0), f(s(z1), f(s(s(z2)), f(x2, x3)))), F(s(z1), f(s(s(z2)), f(x2, x3))), F(s(s(z2)), f(x2, x3)))
L'(f(s(s(x0)), f(s(z0), f(s(z1), f(z2, z3))))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(z2), z3)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), f(z2, z3))))), F(x0, f(s(s(z0)), f(s(z1), f(z2, z3)))), F(s(s(z0)), f(s(z1), f(z2, z3))))
L'(f(s(s(x0)), f(s(z0), f(s(z1), nil)))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(0), nil)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), nil)))), F(x0, f(s(s(z0)), f(s(z1), nil))), F(s(s(z0)), f(s(z1), nil)))
L'(f(s(s(x0)), f(s(x1), f(x2, x3)))) → c2(F(s(0), f(x0, f(s(s(x1)), f(x2, x3)))), F(x0, f(s(s(x1)), f(x2, x3))), F(s(s(x1)), f(x2, x3)))
L'(f(s(s(s(z1))), f(s(z2), nil))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(0), nil))))), F(s(0), f(s(z1), f(s(s(z2)), nil))), F(s(z1), f(s(s(z2)), nil)), F(s(s(z2)), nil))
L'(f(s(s(x0)), f(s(x1), nil))) → c2(F(s(0), f(x0, f(s(s(x1)), nil))), F(x0, f(s(s(x1)), nil)))
S tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
F(x0, f(s(s(x1)), nil)) → c1(F(s(x0), f(x1, f(s(0), nil))))
L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(s(z1))), f(s(z2), f(x2, x3)))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(x2), x3))))), F(s(0), f(s(z1), f(s(s(z2)), f(x2, x3)))), F(s(z1), f(s(s(z2)), f(x2, x3))), F(s(s(z2)), f(x2, x3)))
L'(f(s(s(x0)), f(s(z0), f(s(z1), f(z2, z3))))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(z2), z3)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), f(z2, z3))))), F(x0, f(s(s(z0)), f(s(z1), f(z2, z3)))), F(s(s(z0)), f(s(z1), f(z2, z3))))
L'(f(s(s(x0)), f(s(z0), f(s(z1), nil)))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(0), nil)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), nil)))), F(x0, f(s(s(z0)), f(s(z1), nil))), F(s(s(z0)), f(s(z1), nil)))
L'(f(s(s(s(z1))), f(s(z2), nil))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(0), nil))))), F(s(0), f(s(z1), f(s(s(z2)), nil))), F(s(z1), f(s(s(z2)), nil)), F(s(s(z2)), nil))
K tuples:

L'(f(s(s(x0)), f(x1, x2))) → c2(F(s(x1), x2))
L'(f(s(s(x0)), f(s(x1), f(x2, x3)))) → c2(F(s(0), f(x0, f(s(s(x1)), f(x2, x3)))), F(x0, f(s(s(x1)), f(x2, x3))), F(s(s(x1)), f(x2, x3)))
L'(f(s(s(x0)), f(s(x1), nil))) → c2(F(s(0), f(x0, f(s(s(x1)), nil))), F(x0, f(s(s(x1)), nil)))
Defined Rule Symbols:

f, L

Defined Pair Symbols:

F, L'

Compound Symbols:

c, c1, c2, c2, c2, c2

(17) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(x0, f(s(s(x1)), nil)) → c1(F(s(x0), f(x1, f(s(0), nil)))) by

F(z0, f(s(s(s(s(y1)))), nil)) → c1(F(s(z0), f(s(s(y1)), f(s(0), nil))))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, f(s(s(z1)), f(z2, z3))) → f(s(z0), f(z1, f(s(z2), z3)))
f(z0, f(s(s(z1)), nil)) → f(s(z0), f(z1, f(s(0), nil)))
L(f(s(s(z0)), f(z1, z2))) → L(f(s(0), f(z0, f(s(z1), z2))))
Tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(x0)), f(x1, x2))) → c2(F(s(x1), x2))
L'(f(s(s(s(z1))), f(s(z2), f(x2, x3)))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(x2), x3))))), F(s(0), f(s(z1), f(s(s(z2)), f(x2, x3)))), F(s(z1), f(s(s(z2)), f(x2, x3))), F(s(s(z2)), f(x2, x3)))
L'(f(s(s(x0)), f(s(z0), f(s(z1), f(z2, z3))))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(z2), z3)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), f(z2, z3))))), F(x0, f(s(s(z0)), f(s(z1), f(z2, z3)))), F(s(s(z0)), f(s(z1), f(z2, z3))))
L'(f(s(s(x0)), f(s(z0), f(s(z1), nil)))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(0), nil)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), nil)))), F(x0, f(s(s(z0)), f(s(z1), nil))), F(s(s(z0)), f(s(z1), nil)))
L'(f(s(s(x0)), f(s(x1), f(x2, x3)))) → c2(F(s(0), f(x0, f(s(s(x1)), f(x2, x3)))), F(x0, f(s(s(x1)), f(x2, x3))), F(s(s(x1)), f(x2, x3)))
L'(f(s(s(s(z1))), f(s(z2), nil))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(0), nil))))), F(s(0), f(s(z1), f(s(s(z2)), nil))), F(s(z1), f(s(s(z2)), nil)), F(s(s(z2)), nil))
L'(f(s(s(x0)), f(s(x1), nil))) → c2(F(s(0), f(x0, f(s(s(x1)), nil))), F(x0, f(s(s(x1)), nil)))
F(z0, f(s(s(s(s(y1)))), nil)) → c1(F(s(z0), f(s(s(y1)), f(s(0), nil))))
S tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(s(z1))), f(s(z2), f(x2, x3)))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(x2), x3))))), F(s(0), f(s(z1), f(s(s(z2)), f(x2, x3)))), F(s(z1), f(s(s(z2)), f(x2, x3))), F(s(s(z2)), f(x2, x3)))
L'(f(s(s(x0)), f(s(z0), f(s(z1), f(z2, z3))))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(z2), z3)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), f(z2, z3))))), F(x0, f(s(s(z0)), f(s(z1), f(z2, z3)))), F(s(s(z0)), f(s(z1), f(z2, z3))))
L'(f(s(s(x0)), f(s(z0), f(s(z1), nil)))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(0), nil)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), nil)))), F(x0, f(s(s(z0)), f(s(z1), nil))), F(s(s(z0)), f(s(z1), nil)))
L'(f(s(s(s(z1))), f(s(z2), nil))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(0), nil))))), F(s(0), f(s(z1), f(s(s(z2)), nil))), F(s(z1), f(s(s(z2)), nil)), F(s(s(z2)), nil))
F(z0, f(s(s(s(s(y1)))), nil)) → c1(F(s(z0), f(s(s(y1)), f(s(0), nil))))
K tuples:

L'(f(s(s(x0)), f(x1, x2))) → c2(F(s(x1), x2))
L'(f(s(s(x0)), f(s(x1), f(x2, x3)))) → c2(F(s(0), f(x0, f(s(s(x1)), f(x2, x3)))), F(x0, f(s(s(x1)), f(x2, x3))), F(s(s(x1)), f(x2, x3)))
L'(f(s(s(x0)), f(s(x1), nil))) → c2(F(s(0), f(x0, f(s(s(x1)), nil))), F(x0, f(s(s(x1)), nil)))
Defined Rule Symbols:

f, L

Defined Pair Symbols:

F, L'

Compound Symbols:

c, c2, c2, c2, c2, c1

(19) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace L'(f(s(s(x0)), f(x1, x2))) → c2(F(s(x1), x2)) by

L'(f(s(s(z0)), f(z1, f(s(s(y1)), f(y2, y3))))) → c2(F(s(z1), f(s(s(y1)), f(y2, y3))))
L'(f(s(s(z0)), f(z1, f(s(s(s(s(y1)))), nil)))) → c2(F(s(z1), f(s(s(s(s(y1)))), nil)))

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, f(s(s(z1)), f(z2, z3))) → f(s(z0), f(z1, f(s(z2), z3)))
f(z0, f(s(s(z1)), nil)) → f(s(z0), f(z1, f(s(0), nil)))
L(f(s(s(z0)), f(z1, z2))) → L(f(s(0), f(z0, f(s(z1), z2))))
Tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(s(z1))), f(s(z2), f(x2, x3)))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(x2), x3))))), F(s(0), f(s(z1), f(s(s(z2)), f(x2, x3)))), F(s(z1), f(s(s(z2)), f(x2, x3))), F(s(s(z2)), f(x2, x3)))
L'(f(s(s(x0)), f(s(z0), f(s(z1), f(z2, z3))))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(z2), z3)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), f(z2, z3))))), F(x0, f(s(s(z0)), f(s(z1), f(z2, z3)))), F(s(s(z0)), f(s(z1), f(z2, z3))))
L'(f(s(s(x0)), f(s(z0), f(s(z1), nil)))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(0), nil)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), nil)))), F(x0, f(s(s(z0)), f(s(z1), nil))), F(s(s(z0)), f(s(z1), nil)))
L'(f(s(s(x0)), f(s(x1), f(x2, x3)))) → c2(F(s(0), f(x0, f(s(s(x1)), f(x2, x3)))), F(x0, f(s(s(x1)), f(x2, x3))), F(s(s(x1)), f(x2, x3)))
L'(f(s(s(s(z1))), f(s(z2), nil))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(0), nil))))), F(s(0), f(s(z1), f(s(s(z2)), nil))), F(s(z1), f(s(s(z2)), nil)), F(s(s(z2)), nil))
L'(f(s(s(x0)), f(s(x1), nil))) → c2(F(s(0), f(x0, f(s(s(x1)), nil))), F(x0, f(s(s(x1)), nil)))
F(z0, f(s(s(s(s(y1)))), nil)) → c1(F(s(z0), f(s(s(y1)), f(s(0), nil))))
L'(f(s(s(z0)), f(z1, f(s(s(y1)), f(y2, y3))))) → c2(F(s(z1), f(s(s(y1)), f(y2, y3))))
L'(f(s(s(z0)), f(z1, f(s(s(s(s(y1)))), nil)))) → c2(F(s(z1), f(s(s(s(s(y1)))), nil)))
S tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(s(z1))), f(s(z2), f(x2, x3)))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(x2), x3))))), F(s(0), f(s(z1), f(s(s(z2)), f(x2, x3)))), F(s(z1), f(s(s(z2)), f(x2, x3))), F(s(s(z2)), f(x2, x3)))
L'(f(s(s(x0)), f(s(z0), f(s(z1), f(z2, z3))))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(z2), z3)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), f(z2, z3))))), F(x0, f(s(s(z0)), f(s(z1), f(z2, z3)))), F(s(s(z0)), f(s(z1), f(z2, z3))))
L'(f(s(s(x0)), f(s(z0), f(s(z1), nil)))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(0), nil)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), nil)))), F(x0, f(s(s(z0)), f(s(z1), nil))), F(s(s(z0)), f(s(z1), nil)))
L'(f(s(s(s(z1))), f(s(z2), nil))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(0), nil))))), F(s(0), f(s(z1), f(s(s(z2)), nil))), F(s(z1), f(s(s(z2)), nil)), F(s(s(z2)), nil))
F(z0, f(s(s(s(s(y1)))), nil)) → c1(F(s(z0), f(s(s(y1)), f(s(0), nil))))
K tuples:

L'(f(s(s(x0)), f(s(x1), f(x2, x3)))) → c2(F(s(0), f(x0, f(s(s(x1)), f(x2, x3)))), F(x0, f(s(s(x1)), f(x2, x3))), F(s(s(x1)), f(x2, x3)))
L'(f(s(s(x0)), f(s(x1), nil))) → c2(F(s(0), f(x0, f(s(s(x1)), nil))), F(x0, f(s(s(x1)), nil)))
L'(f(s(s(z0)), f(z1, f(s(s(y1)), f(y2, y3))))) → c2(F(s(z1), f(s(s(y1)), f(y2, y3))))
L'(f(s(s(z0)), f(z1, f(s(s(s(s(y1)))), nil)))) → c2(F(s(z1), f(s(s(s(s(y1)))), nil)))
Defined Rule Symbols:

f, L

Defined Pair Symbols:

F, L'

Compound Symbols:

c, c2, c2, c2, c1, c2

(21) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 2 leading nodes:

L'(f(s(s(z0)), f(z1, f(s(s(s(s(y1)))), nil)))) → c2(F(s(z1), f(s(s(s(s(y1)))), nil)))
L'(f(s(s(z0)), f(z1, f(s(s(y1)), f(y2, y3))))) → c2(F(s(z1), f(s(s(y1)), f(y2, y3))))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, f(s(s(z1)), f(z2, z3))) → f(s(z0), f(z1, f(s(z2), z3)))
f(z0, f(s(s(z1)), nil)) → f(s(z0), f(z1, f(s(0), nil)))
L(f(s(s(z0)), f(z1, z2))) → L(f(s(0), f(z0, f(s(z1), z2))))
Tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(s(z1))), f(s(z2), f(x2, x3)))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(x2), x3))))), F(s(0), f(s(z1), f(s(s(z2)), f(x2, x3)))), F(s(z1), f(s(s(z2)), f(x2, x3))), F(s(s(z2)), f(x2, x3)))
L'(f(s(s(x0)), f(s(z0), f(s(z1), f(z2, z3))))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(z2), z3)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), f(z2, z3))))), F(x0, f(s(s(z0)), f(s(z1), f(z2, z3)))), F(s(s(z0)), f(s(z1), f(z2, z3))))
L'(f(s(s(x0)), f(s(z0), f(s(z1), nil)))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(0), nil)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), nil)))), F(x0, f(s(s(z0)), f(s(z1), nil))), F(s(s(z0)), f(s(z1), nil)))
L'(f(s(s(x0)), f(s(x1), f(x2, x3)))) → c2(F(s(0), f(x0, f(s(s(x1)), f(x2, x3)))), F(x0, f(s(s(x1)), f(x2, x3))), F(s(s(x1)), f(x2, x3)))
L'(f(s(s(s(z1))), f(s(z2), nil))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(0), nil))))), F(s(0), f(s(z1), f(s(s(z2)), nil))), F(s(z1), f(s(s(z2)), nil)), F(s(s(z2)), nil))
L'(f(s(s(x0)), f(s(x1), nil))) → c2(F(s(0), f(x0, f(s(s(x1)), nil))), F(x0, f(s(s(x1)), nil)))
F(z0, f(s(s(s(s(y1)))), nil)) → c1(F(s(z0), f(s(s(y1)), f(s(0), nil))))
S tuples:

F(z0, f(s(s(z1)), f(z2, z3))) → c(F(s(z0), f(z1, f(s(z2), z3))), F(z1, f(s(z2), z3)), F(s(z2), z3))
L'(f(s(s(s(s(z1)))), f(x1, z3))) → c2(L'(f(s(s(0)), f(z1, f(s(s(x1)), z3)))), F(s(0), f(s(s(z1)), f(s(x1), z3))), F(s(s(z1)), f(s(x1), z3)), F(s(x1), z3))
L'(f(s(s(s(z1))), f(s(z2), f(x2, x3)))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(x2), x3))))), F(s(0), f(s(z1), f(s(s(z2)), f(x2, x3)))), F(s(z1), f(s(s(z2)), f(x2, x3))), F(s(s(z2)), f(x2, x3)))
L'(f(s(s(x0)), f(s(z0), f(s(z1), f(z2, z3))))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(z2), z3)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), f(z2, z3))))), F(x0, f(s(s(z0)), f(s(z1), f(z2, z3)))), F(s(s(z0)), f(s(z1), f(z2, z3))))
L'(f(s(s(x0)), f(s(z0), f(s(z1), nil)))) → c2(L'(f(s(0), f(s(x0), f(s(z0), f(z1, f(s(0), nil)))))), F(s(0), f(x0, f(s(s(z0)), f(s(z1), nil)))), F(x0, f(s(s(z0)), f(s(z1), nil))), F(s(s(z0)), f(s(z1), nil)))
L'(f(s(s(s(z1))), f(s(z2), nil))) → c2(L'(f(s(s(0)), f(z1, f(s(z2), f(s(0), nil))))), F(s(0), f(s(z1), f(s(s(z2)), nil))), F(s(z1), f(s(s(z2)), nil)), F(s(s(z2)), nil))
F(z0, f(s(s(s(s(y1)))), nil)) → c1(F(s(z0), f(s(s(y1)), f(s(0), nil))))
K tuples:

L'(f(s(s(x0)), f(s(x1), f(x2, x3)))) → c2(F(s(0), f(x0, f(s(s(x1)), f(x2, x3)))), F(x0, f(s(s(x1)), f(x2, x3))), F(s(s(x1)), f(x2, x3)))
L'(f(s(s(x0)), f(s(x1), nil))) → c2(F(s(0), f(x0, f(s(s(x1)), nil))), F(x0, f(s(s(x1)), nil)))
Defined Rule Symbols:

f, L

Defined Pair Symbols:

F, L'

Compound Symbols:

c, c2, c2, c2, c1

(23) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 0.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2]
transitions:
s0(0) → 0
00() → 0
nil0() → 0
f0(0, 0) → 1
L0(0) → 2

(24) BOUNDS(O(1), O(n^1))